#ifndef PROGRAM_SLICING_HPP
#define	PROGRAM_SLICING_HPP

#include <set>
#include "monotone_framework.hpp"
using namespace std;



class program_slicing {
public:
	program_slicing(const CFGvisitorFlatInfo& _flat, const ReachingDefs& _rd);
	void pslice(label_t ell0);
	set<label_t> getS() const;

private:
	void mark_as_visited(label_t ell);
	bool has_been_visited(label_t ell);
	set<string/*var*/> used(label_t ell) const;
	ASTnode* getPayload(label_t ell0) const;
	ASTnode* getPayload(CFGvertex *n) const;
	set<label_t> get_nested_If_and_Whiles(label_t ell0) const;
	
	vector<bool> visited;
	set<label_t> S;
	const CFGvisitorFlatInfo& flat;
	const ReachingDefs& rd;
};

#endif	/* PROGRAM_SLICING_HPP */

